Step of Proof: top_wf
12,41
postcript
pdf
Inference at
*
I
of proof for Lemma
top
wf
:
Top
Type
latex
by Unfold `top` 0
latex
1
:
1:
(
x
:Void.Void)
Type
.
Definitions
Top
origin
Top 
Type
by Unfold `top` 0
1:
1: (
x:Void.Void) Type
. Top Type
by Unfold `top` 0
1:
1: (x:Void.Void) Type
.